Step of Proof: not_assert_elim
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
not
assert
elim
:
b
:
. (
(
b
))
(
b
= ff)
latex
by ((UnivCD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
1.
b
:
C1:
2.
(
b
)
C1:
b
= ff
C
.
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
bool
wf
,
assert
wf
,
not
wf
origin